Method withdraw(提款)

此方法為簽名後執行提款如下定義：

fun withdraw<CoinType>(addr: address, amount: u64) : Coin<CoinType> acquires Balance

從addr中提取具有價值的tokens，並傳回一個創建的價值為Coin的數量。
執行提款時當

1. addr沒有資源Balance 或 2) 在addr中的token的數量小於amount時，此方法將中止。我們可以這樣定義條件：

    spec withdraw {
        let balance = global<Balance<CoinType>>(addr).coin.value;
        aborts_if !exists<Balance<CoinType>>(addr);
        aborts_if balance < amount;
    }

正如我們在這裡看到的，spec 區塊可以包含引入表達式名稱的 let 綁定。
global(address): T是內建函數，傳回處的資源值addr。balance是擁有的代幣數量addr。
exists(address): bool是內建函數，如果位址處存在資源 T，則傳回 true。
兩個aborts_if子句分別對應上述兩個條件。
一般來說，如果一個函數有多個aborts_if條件，這些條件就會互相進行或運算。
預設情況下，如果使用者想要指定中止條件，則需要列出所有可能的條件。
否則，驗證器將產生驗證錯誤。
但是，如果pragma aborts_if_is_partial在規範區塊中定義，則組合中止條件（or-ed 單獨條件）僅表示此函數中止。可以參考 MSL文件了解更多。

下一步是定義功能屬性，這在ensures下面的兩個條款中進行了描述。首先，透過使用let post綁定，balance_post表示執行後的餘額addr，應等於balance - amount。那麼，傳回值（表示為result）應該是一個值為的硬幣amount。

    spec withdraw {
        let balance = global<Balance<CoinType>>(addr).coin.value;
        aborts_if !exists<Balance<CoinType>>(addr);
        aborts_if balance < amount;

        let post balance_post = global<Balance<CoinType>>(addr).coin.value;
        ensures balance_post == balance - amount;
        ensures result == Coin<CoinType> { value: amount };
    } 

Method deposit(存款)

此方法的簽名deposit如下：

fun deposit<CoinType>(addr: address, check: Coin<CoinType>) acquires Balance

該方法將check存入addr。該規範定義如下：

    spec deposit {
        let balance = global<Balance<CoinType>>(addr).coin.value;
        let check_value = check.value;

        aborts_if !exists<Balance<CoinType>>(addr);
        aborts_if balance + check_value > MAX_U64;

        let post balance_post = global<Balance<CoinType>>(addr).coin.value;
        ensures balance_post == balance + check_value;
    }

balanceaddr代表執行前的代幣Coin數量，check_value代表待存入的代幣數量。如果 1)addr沒有資源Balance 或 2)balance及check_value的總和大於類型u64的最大值，則該方法將中止。功能屬性檢查執行後餘額是否正確更新。

Method transfer(轉帳)

簽證後的transfer方法如下：

public fun transfer<CoinType: drop>(from: &signer, to: address, amount: u64, _witness: CoinType) acquires Balance

此方法將 的amount幣從 的 帳戶轉移from到地址to。規格如下：

    spec transfer {
        let addr_from = signer::address_of(from);

        let balance_from = global<Balance<CoinType>>(addr_from).coin.value;
        let balance_to = global<Balance<CoinType>>(to).coin.value;
        let post balance_from_post = global<Balance<CoinType>>(addr_from).coin.value;
        let post balance_to_post = global<Balance<CoinType>>(to).coin.value;

        ensures balance_from_post == balance_from - amount;
        ensures balance_to_post == balance_to + amount;
    }

addr_from是 的位址from。然後得到執行前後addr_from的餘額。to這些ensures子句指定從 中扣除和新增amount令牌數量。但是，證明者會產生以下錯誤訊息：addr_fromto

error: post-condition does not hold
   ┌─ ./sources/BasicCoin.move:57:9
   │
62 │         ensures balance_from_post == balance_from - amount;
   │         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
   │
   ...

addr_from當等於 時，不持有該財產to。因此，我們可以assert!(from_addr != to)在方法中加入一個斷言以確保addr_from不等於to。